$\forall$$T$, $I$:Type, $L$:($I$$\rightarrow$($T$ List)), $L_{2}$:$T$ List. interleaved\_family($T$;$I$;$L$;$L_{2}$) $\in$ Prop